Skip to content

Split ci-ubuntu workflow into multiple jobs#3049

Draft
silas-hw wants to merge 21 commits into
agda:masterfrom
silas-hw:optimise-ci
Draft

Split ci-ubuntu workflow into multiple jobs#3049
silas-hw wants to merge 21 commits into
agda:masterfrom
silas-hw:optimise-ci

Conversation

@silas-hw

@silas-hw silas-hw commented Jul 2, 2026

Copy link
Copy Markdown
Contributor

ci-ubuntu can be split up into multiple jobs which run in parallel. This also potentially leads the way to further CI improvements. Currently I've split doc related steps and testing related steps to run in parallel. It may also be possible for golden testing to run in parallel to standard tests.

GitHub Actions is a bit of a pain in that there's no way to have some way of setting up an initial workspace for each job to run in. This means that the init steps (set up env, install things, etc...) have to run on every job. To reduce redundant code I split this out into a composite workflow (see https://docs.github.com/en/actions/tutorials/create-actions/create-a-composite-action). This action will be given all the env variables set up by the calling workflow and can likewise set them with the usual write to GITHUB_ENV (see https://github.com/orgs/community/discussions/51280#discussioncomment-8726096).

I'm still not fully confident on this though.

@silas-hw

silas-hw commented Jul 2, 2026

Copy link
Copy Markdown
Contributor Author

Seems checkout needs to run first

@gallais

gallais commented Jul 2, 2026

Copy link
Copy Markdown
Member

That summary looks concerning: https://github.com/agda/agda-stdlib/actions/runs/28607124313?pr=3049
In case of cache miss, it looks like you'll rebuild Agda twice (in parallel but that's still wasteful).

I would recommend looking at the structure of the Idris2 CI pipeline:
https://github.com/idris-lang/Idris2/blob/main/.github/workflows/ci-idris2-and-libs.yml

You can see from the summary https://github.com/idris-lang/Idris2/actions/runs/28065704913?pr=3775
that we have a clear dependency graph & reuse artifacts produced in one stage in the later ones
(via actions/upload-artifact@v4).

So you could have a first stage checking whether we have agda in the cache. If not, build it and upload it.
Then have testing and upload the agdai files for the lib.
Then have in parallel golden testing & html generation.
Then deploy the html only if we are in the right branch and everything succeeded.

@silas-hw

silas-hw commented Jul 2, 2026

Copy link
Copy Markdown
Contributor Author

Seems a much better approach indeed. Initially dismissed upload-artificact since it seemed more tedious than needed, but given more thought it seems significantly more reasonable.

@silas-hw

silas-hw commented Jul 2, 2026

Copy link
Copy Markdown
Contributor Author

GITHUB_PATH is only for writing by the looks of it, fixing that now

@silas-hw

silas-hw commented Jul 2, 2026

Copy link
Copy Markdown
Contributor Author

Right now I don't like how sudo is before 'chmod' and that it's done on entire folders. Unsure if it should be changed, but chmod without sudo results in 'operation not permitted' due to how upload- and download- artifact handles permissions.

I imagine it would also be best to delete the artifacts after the workflow run?

Sorry for the large number of 'fix' commits. It's been a while since I've handled GitHub Actions.

@silas-hw

silas-hw commented Jul 2, 2026

Copy link
Copy Markdown
Contributor Author

So you could have a first stage checking whether we have agda in the cache. If not, build it and upload it. Then have testing and upload the agdai files for the lib. Then have in parallel golden testing & html generation. Then deploy the html only if we are in the right branch and everything succeeded.

@gallais It can't seem to find the agdai files. Am I doing something obviously wrong? I presume wildcards with upload-artifact work differently to how I think they do.

HTML is all in one job still, but I'll split out deploying it tomorrow.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants